introduce binding_exprt [blocks: #4510] #4931

kroening · 2019-07-20T14:43:10Z

This is a base class that factors out some common functionality of various
expressions that are variable bindings; examples are let, lambda, forall,
exists; future additions might include choose.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov-io · 2019-07-20T17:09:38Z

Codecov Report

Merging #4931 into develop will increase coverage by <.01%.
The diff coverage is 97.36%.

@@             Coverage Diff             @@
##           develop    #4931      +/-   ##
===========================================
+ Coverage    69.24%   69.25%   +<.01%     
===========================================
  Files         1309     1309              
  Lines       108476   108499      +23     
===========================================
+ Hits         75117    75141      +24     
+ Misses       33359    33358       -1

Impacted Files	Coverage Δ
src/ansi-c/expr2c_class.h	`100% <ø> (ø)`	⬆️
src/util/mathematical_expr.h	`93.1% <100%> (+2.62%)`	⬆️
src/ansi-c/c_typecheck_expr.cpp	`72.55% <100%> (+0.02%)`	⬆️
src/ansi-c/parser.y	`78.08% <100%> (ø)`	⬆️
src/solvers/smt2/smt2_parser.cpp	`65.43% <100%> (ø)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`59.62% <100%> (+0.03%)`	⬆️
src/ansi-c/expr2c.cpp	`67.13% <85.71%> (ø)`	⬆️
.../goto-instrument/accelerate/acceleration_utils.cpp	`0% <0%> (ø)`	⬆️
src/solvers/flattening/boolbv_quantifier.cpp	`91.89% <0%> (+0.11%)`	⬆️
... and 2 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 602e2e8...190f1c8. Read the comment docs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ce8b26c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119891946

smowton

Why don't the users (e.g. typecheck_expr_main) use the newly-introduced interface instead of the pretty-opaque expr.op0().op0().op0()?

smowton · 2019-07-23T10:21:15Z

src/solvers/flattening/boolbv_quantifier.cpp

@@ -145,14 +140,14 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
    return re;
  }

-  const exprt min_i = get_quantifier_var_min(var_expr, re);
-  const exprt max_i = get_quantifier_var_max(var_expr, re);
+  const auto min_i = get_quantifier_var_min(var_expr, re);


use constant_exprt, nothing else here makes it obvious we're talking about a constant

tautschnig

These .op0() chains are very opaque and make it rather impossible to understand what's going on. And then wouldn't we really also need to make some changes in the back-end now that the structure of those expressions is different? And the commit message talks about lambdas, lets, but only quantifiers received this new treatment. I don't think we should do half-a-job here.

kroening · 2019-08-05T14:10:46Z

I've introduce further typing to reduce the op0() chains.
Note that we don't have lamba expressions yet, so this PR can't change them.

tautschnig · 2019-08-05T14:14:33Z

Note that we don't have lamba expressions yet, so this PR can't change them.

Well, we have array_comprehension_exprt (with id() == ID_lambda).

kroening · 2019-08-05T14:21:15Z

I'll clean up array_comprehension_exprt vs. Church's lamba_exprt in a follow-up PR; this should not be done here.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 190f1c8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121976290

tautschnig · 2019-08-05T19:02:36Z

src/util/mathematical_expr.h

+
+  variablest &variables()
+  {
+    return (variablest &)static_cast<tuple_exprt &>(op0()).operands();


Quite likely this isn't the only such place, but this clearly makes USE_LIST no longer possible -- but in this case without causing compilation errors. So should we really get rid of USE_LIST right now?

It would be possible to make this work with USE_LIST. Is USE_LIST sill useful?

The code wouldn't actually compile with USE_LIST. If USE_LIST were to work, we could change irept to have only a single container and some cursor(s) into that. Whether that's more efficient or not I can't tell, because it wouldn't compile...

This is a base class that factors out some common functionality of various expressions that are variable bindings; examples are let, lambda, forall, exists; future additions might include choose.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3243b98).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122132439
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

This commit makes the quantifier base class use the bindings base class. Methods and constructor for the special case of quantifying over one variable are retained.

@smowton

This clarifies that the expression returned by get_quantifier_var_min is a constant -- request by @smowton.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 0983a0c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122168140
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0983a0c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122168140

kroening added the cleanup label Jul 20, 2019

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners July 20, 2019 14:43

kroening force-pushed the binding branch from c28e9f4 to ce8b26c Compare July 20, 2019 16:16

allredj reviewed Jul 20, 2019

View reviewed changes

kroening force-pushed the binding branch 2 times, most recently from 335fb5c to f13b9d7 Compare July 22, 2019 01:04

kroening requested a review from martin-cs as a code owner July 22, 2019 01:04

smowton reviewed Jul 23, 2019

View reviewed changes

kroening mentioned this pull request Jul 27, 2019

prop_conv_solvert: introduce scopes #4510

Merged

5 tasks

kroening force-pushed the binding branch from f13b9d7 to 19ea6c3 Compare August 5, 2019 08:26

tautschnig requested changes Aug 5, 2019

View reviewed changes

tautschnig assigned kroening Aug 5, 2019

tautschnig changed the title ~~introduce binding_exprt~~ introduce binding_exprt [blocks: #4510] Aug 5, 2019

tautschnig added the blocker label Aug 5, 2019

kroening force-pushed the binding branch 2 times, most recently from f4a41ab to 1895684 Compare August 5, 2019 13:56

kroening requested a review from romainbrenguier as a code owner August 5, 2019 13:56

kroening force-pushed the binding branch 2 times, most recently from 225d1cf to 4386617 Compare August 5, 2019 14:10

kroening force-pushed the binding branch from 4386617 to 190f1c8 Compare August 5, 2019 14:14

allredj reviewed Aug 5, 2019

View reviewed changes

kroening assigned tautschnig and unassigned kroening Aug 5, 2019

tautschnig approved these changes Aug 5, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Aug 5, 2019

introduce binding_exprt

4dd483a

This is a base class that factors out some common functionality of various expressions that are variable bindings; examples are let, lambda, forall, exists; future additions might include choose.

kroening force-pushed the binding branch from 3243b98 to c3a69a4 Compare August 6, 2019 14:50

allredj reviewed Aug 6, 2019

View reviewed changes

Daniel Kroening added 2 commits August 6, 2019 19:01

quantifiers are variable bindings

c4f7a89

This commit makes the quantifier base class use the bindings base class. Methods and constructor for the special case of quantifying over one variable are retained.

make return type of get_quantifier_var_min obvious

0983a0c

This clarifies that the expression returned by get_quantifier_var_min is a constant -- request by @smowton.

kroening force-pushed the binding branch from c3a69a4 to 0983a0c Compare August 6, 2019 18:02

allredj reviewed Aug 6, 2019

View reviewed changes

kroening merged commit 9a3ffde into develop Aug 6, 2019

kroening deleted the binding branch August 6, 2019 20:48

introduce binding_exprt [blocks: #4510] #4931

introduce binding_exprt [blocks: #4510] #4931

Uh oh!

Conversation

kroening commented Jul 20, 2019

Uh oh!

codecov-io commented Jul 20, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Jul 23, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Aug 5, 2019

Uh oh!

tautschnig commented Aug 5, 2019

Uh oh!

kroening commented Aug 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 6, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 7, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Jul 20, 2019 •

edited

Loading